COMMENT ⊗   VALID 00007 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "lspmac.pub[lsp,clt]" source
C00003 00003	.hd206 Fall 1977
C00006 00004	.bb  Problem 1.
C00013 00005	.bb Problem 2.
C00025 00006	.bb Problem 3.
C00031 00007
C00032 ENDMK
C⊗;
.require "lspmac.pub[lsp,clt]" source;
.LSPFONT 
.allop 
.basicops 
.MACRO  hd206 (TERM) ⊂
.BEGIN    NOFILL  TURNON "←→"
←COMPUTER SCIENCE DEPARTMENT
←STANFORD UNIVERSITY
.SKIP  
CS206  ←COMPUTING WITH SYMBOLIC EXPRESSIONS  →TERM
.TURNOFF
.END ⊃
.
.itemmac
.PORTION MAINPORTION
.PAGE ← 1
.hd206 Fall 1977
.cb Solutions for Problem Set 2.

.bb General comments.

	The homework indicates that people seem to be able to use the two
inductions schemas and work out the main steps of a proof.  The main
difficulty seems to be in understanding how to use the fact that some 
of the variables have restricted ranges (are sorted).
Since the axioms are stated in terms of sorted variables it is important
to understand the implications of this in order not to prove things
which are in fact false.  Therefore in presenting the 
solutions to problems 1 and 2, I will try to be especially carefull to point 
out where it is that terms have to
be shown to be of a given sort in order for the axioms, definitions, and
theorems can be applied.  
The proofs will be fairly brief in other respects
and in particular the basic LISP axioms will often used without comment.
Hopefully this together with the revised section of Chapter 3 
will help make this style of proof clearer.   

	Problem 3 is worked out in some detail as many people did not
make a formal connection between the imitation and real predicates  and
other details were frequently missed.

	In grading the homework, I looked for correctness of the steps of
each proof and indicated places where although the proof step was correct
some of the necessary facts had not been established.  No number grade
was given.  If there are points which you still are not sure of please ask.

.bb  Problem 1.

	We will use the following facts about the operator < >: 

1.0		⊗⊗∀x: islist <x>⊗   and    ⊗⊗∀x u: <x> * u = x . u⊗

We will use the fact that 
⊗⊗issexp qa u⊗ and ⊗⊗issexp qd u⊗ in the case that ⊗⊗¬qn u⊗ 
often without explicit mention.
These facts are a simple consequence of the definitions of *, <> and the LISP axioms.  
We will also use the result of Problem 1.i which was proved in class.  We will
sometimes justify a step saying "by definition"  which means by whatever function
definition is relevant.

.bb |Proof of 1.ii         ⊗⊗∀u: islist reverse1 u⊗|
.nofill

Method:	list induction with   ⊗⊗qP[u] ≡ islist reverse1 u⊗.  

Case ⊗⊗qn u⊗:

    ⊗⊗islist reverse1 u ≡ islist qNIL⊗    ...by definition of ⊗reverse1 
                        ≡ T   ...by the LISP axioms.

Case  ⊗⊗¬qn u⊗ and ⊗⊗islist_reverse1_qd u⊗ 

    ⊗⊗islist reverse1 u ≡ islist [reverse1_qd u_*_<qa u>]⊗   ...by definition  of ⊗reverse1 
                        ≡  T   ...by induction hypothesis, $ISLIST-APPEND and 1.0.

.bb |Proof of 1.iii  ⊗⊗∀u: reverse u = reverse1 u⊗|
	We prove a slightly more general result, namely

1.1		⊗⊗∀u v: reverse1 u * v = rev[u,v]⊗

then taking ⊗v = qNIL the desired result follows by 1.i  and the definition of ⊗reverse.  

Method: list induction with   ⊗⊗qP[u]_≡_∀v:_reverse1_u_*_v_=_rev[u,v]⊗.  

Case  ⊗⊗qn u⊗ 

    ⊗⊗reverse1 qNIL * v = v⊗   ...by definition of ⊗reverse1 and $NIL-APPEND 
                      ⊗⊗= rev[u,v]⊗   ...by definition of ⊗rev .

Case  ⊗⊗¬qn u⊗ and ⊗⊗∀v:_reverse1_qd u_*_v_=_rev[qd u,v]⊗:

    ⊗⊗reverse1 u = reverse1 qd u * <qa u>⊗   ...by definition
		    ⊗⊗= rev[qd u,<qa u>]⊗   ...by induction hypothesis and ⊗⊗islist <qa u>⊗
		    ⊗⊗= rev[u,qNIL]⊗   ...by definition.

From here on we shall use ⊗reverse and ⊗reverse1 interchangably.

.bb |Proof of 1.v  ⊗⊗∀u v: [reverse[u * v] = reverse v * reverse u]⊗ |
Method: list induction with ⊗⊗qP[u] ≡ ∀v: reverse[u * v] = reverse v * reverse u]⊗. 

Case ⊗⊗qn u⊗:

    ⊗⊗reverse[qNIL * v] = reverse v⊗   ...by $NIL-APPEND  
                   ⊗⊗= reverse v * qNIL⊗   ...by 1.i
                   ⊗⊗= reverse v * reverse qNIL⊗   ...by definition.

Case	⊗⊗¬qn u⊗ and ⊗⊗∀v:_reverse[qd u * v]_=_reverse v * reverse qd u⊗:

    ⊗⊗reverse[u * v] = reverse[qd u * v] * <qa u>⊗   ...by definition, $CAR/CDR-APPEND and ⊗⊗islist u*v⊗
		    ⊗⊗= [reverse v * reverse qd u] * <qa u>⊗   ...by induction hypothesis
		    ⊗⊗= reverse v * [reverse qd u * <qa u>]⊗   ...by $ASSOC-APPEND 
		...here we need ⊗⊗islist reverse v⊗, ⊗⊗islist reverse qd u⊗ and ⊗⊗islist <qa u>⊗
		    ⊗⊗= reverse v * reverse u⊗   ...by definition
 
.bb |Proof of 1.iv   ⊗⊗∀u: reverse reverse u = u⊗ |
Method: list induction with    ⊗⊗qP[u] ≡ reverse reverse u = u⊗.  

Case ⊗⊗qn u⊗:

    ⊗⊗reverse reverse qNIL = reverse qNIL = qNIL⊗   ... by definition

Case    ⊗⊗¬qn u⊗ and ⊗⊗reverse_reverse_qd u_=_qd u⊗:

    ⊗⊗reverse reverse u = reverse[reverse qd u * <qa u>]⊗   ...by definition
		    ⊗⊗= reverse <qa u> * reverse reverse qd u⊗   ... by 1.v
             ...here we need ⊗⊗islist reverse qd u⊗ and ⊗⊗islist <qa u>⊗
		    ⊗⊗= <qa u> * qd u⊗   ...by induction hypothesis and computation  using ⊗⊗islist <qa u>⊗
		    ⊗⊗= u⊗   ...by 1.0 and the LISP axioms

.bb |Proof of the ⊗fringe problem  ⊗⊗⊗∀x u: flat[x,u] = fringe x * u⊗|
Method: S-expression induction with   ⊗⊗qP[x]_≡_∀u:_flat[x,u]_=_fringe_x_*_u⊗.  

Case ⊗⊗qat x⊗:

    ⊗⊗flat[x,u]_=_x_._u⊗    ...by definition
              ⊗⊗= <x> * u⊗   ... by 1.0
              ⊗⊗= fringe x * u⊗  ... by definition

Case   ⊗⊗¬qat x⊗ and ⊗⊗∀u:_flat[qd x,u]_=_fringe_qd x_*_u⊗ :

    ⊗⊗flat[x,u] = flat[qa x,flat[qd x,u]]⊗   ...by definition
		    ⊗⊗= flat[qa x,fringe qd x * u]⊗   ...by induction hypothesis
		    ⊗⊗= fringe qa x * [fringe qd x * u]⊗   ...again by induction hypothesis
                                            ...here we need ⊗⊗islist fringe qd x * u⊗
		    ⊗⊗= fringe x * u⊗   ...by $ISTOT-APPEND and definition of ⊗fringe  
                           ...here we need ⊗⊗islist fringe qd x ⊗ and ⊗⊗islist fringe qa x⊗

This ends Problem 1.
.fill

.bb Problem 2.

	In proving the desired fact about ⊗subst, ⊗sublis, and @ we will use a new
sort ⊗slist.  The variables ⊗s, ⊗s1, ⊗s2, ⊗s3 range over the domain 
characterized by the predicate ⊗slist.  We axiomatize slists as follows:

2.1 	⊗⊗∀X: [slist X ≡ islist X ∧ [qn X ∨ [¬qat qa X ∧ slist qd X]]]⊗   ...X is a general variable.

Thus ⊗s is either qNIL or a list of nonatomic elements.   We shall also use the
following facts.
.nofill

2.2	⊗⊗∀x y: [occur[x,y] ≡ [x=y] ∨ [¬qat y ∧ [occur[x, qa y] ∨ occur[x,qd y]]]]⊗
2.3	⊗⊗∀x s: [qn assoc[x,s] ∨ [issexp assoc[x,s] ∧ ¬qat assoc[x,s]]]⊗
2.4     ⊗⊗∀s1 s2:  slist s1 * s2⊗
2.5	⊗⊗∀z s1 s2: [assoc[z,s1*s2] = qif qn assoc[z,s1] qthen assoc[z,s2] qelse assoc[z,s1]]⊗
2.6	⊗⊗∀x y z: issexp subst[x, y, z]⊗
2.7	⊗⊗∀x,s: issexp sublis[x,s]⊗
2.8	⊗⊗∀s1 s2: slist subsub[s1,s2]⊗
	⊗⊗∀s1 s2:  ¬qn s1 ⊃ ¬qn subsub[s1,s2]⊗
	⊗⊗∀s1 s2:  ¬qn s1 ⊃ qd subsub[s1,s2] = subsub[qd s1,s2]⊗
2.9	⊗⊗∀s1 s2: slist s1@s2⊗
.fill
The proof of 2.2 is outlined in the notes and 2.3 - 2.9 can be proved by 
straight forward list or S-expression induction using the LISP axioms 
function definitions and 2.1.

.bb |Proof of 2.i   ⊗⊗∀x y z: subst[x, y, z] = sublis[z, <x,y>]⊗ |
.nofill

Method: S-expression induction with   ⊗⊗qP[z]_≡_∀x_y:_subst[x,y,z]_=_sublis[z,<x.y>]⊗. 

Case ⊗⊗qat z⊗:

    ⊗⊗subst[x,y,z] = qif y=z qthen x qelse z⊗    ...by definition of ⊗subst 
    ⊗⊗sublis[z,<y.x>] = {assoc[z,<y.x>]}[λz1: qif qn z1 qthen z qelse qd z1]⊗   ... by definition of ⊗sublis 
		    ⊗⊗= qif y≠z qthen z qelse qd y.x⊗    ...by computation since ⊗⊗slist <y.x>⊗.

Case ⊗⊗¬qat z⊗ and ⊗⊗∀x y: [subst[x, y, qa z] = sublis[qa z, <y.x>] ∧ subst[x,y,qd z] = sublis[qd z,<y.x>]]⊗

    ⊗⊗subst[x,y,z] = subst[x,y,qa z] . subst[x,y,qd z]⊗    ...by definition of ⊗subst 
		    ⊗⊗= sublis[qa z, <y.x>] . sublis[qd z,<y.x>]⊗    ...by induction hypothesis
		    ⊗⊗= sublis[z,<y.x>]⊗    ...by definition of ⊗sublis.  


	Before proving (ii) we prove some lemmas.  Namely

2.10	⊗⊗∀z s1 s2: [qn assoc[z, s1] ⊃ assoc[z, s1@s2] = assoc[z,s2]]⊗
2.11	⊗⊗∀z s1 s2:  [¬qn assoc[z,s1] ⊃ ¬qn assoc[z,s1@s2] ∧ qd assoc[z,s1@s2] = sublis[qd assoc[z,s1],s2]⊗
.fill

These are fairly simple consequences of the facts mentioned at the beginning of 
this problem and the following statement:
.nofill

2.12	⊗⊗∀z s1 s2: [qn assoc[z, s1] ≡ qn assoc[z,subsub[s1,s2]]]⊗
		⊗⊗∧ [¬qn assoc[z,s1] ⊃ qd assoc[z,subsub[s1,s2] = sublis[qd assoc[z,s1],s2]]⊗

.bb |Proof of 2.12.|
Method:  list induction on ⊗s1.  

Case ⊗⊗qn s1⊗:  

    Both sides of the equivalence reduce to ⊗⊗qn qNIL⊗ and the left hand side of ⊃ is F. 


Case ⊗⊗¬qn s1⊗ and ⊗⊗∀z s2: [qn assoc[z, qd s1] ≡ qn assoc[z,subsub[qd s1,s2]]]⊗
                   ⊗⊗∀z s2: [¬qn assoc[z,qd s1] ⊃ qd assoc[z,subsub[qd s1,s2] = sublis[qd assoc[z,qd s1], s2]]⊗

    ⊗⊗assoc[z,subsub[s1,s2]] = qif z=qaa subsub[s1,s2] qthen qa subsub[s1,s2] qelse assoc[z,subsub[qd s1,s2]]⊗ 
           ...by definition of ⊗assoc 
           ...here we need ⊗⊗slist subsub[s1,s2]⊗, ⊗⊗¬qn subsub[s1,s2]⊗ and ⊗⊗qd subsub[s1,s2] = subsub[qd s1,s2]⊗
		⊗⊗= qif z = qaa s1 qthen [qaa s1 . sublis[qda s1,s2]] qelse assoc[z, subsub[qd s1,s2]]⊗
           ...here we need in addition, 2.1, the definition of ⊗subsub and ⊗⊗issexp sublis[qda s1,s2]⊗

Subcase  ⊗⊗z = qaa s1 ⊗:  the result follows from the definitions by computation.

Subcase   ⊗⊗z ≠ qaa s1⊗: the result follows from the induction hypothesis and definition of ⊗assoc.  

.bb |Proof of 2.10|
Assume: ⊗⊗qn assoc[z,s1]⊗ 

    ⊗⊗qn assoc[z, subsub[s1,s2]]⊗    ... by 2.12
    ⊗⊗assoc[z,subsub[s1,s2]*s2]_=_assoc[z,s1@s2]_=_assoc[z,s2]⊗   ...by 2.5 and definition of @. 

.bb |Proof of 2.11|
Assume: ⊗⊗¬qn assoc[z,s1]⊗ 

    ⊗⊗¬qn assoc[z,subsub[s1,s2]]⊗    ...by 2.12
    ⊗⊗assoc[z,s1@s2]_=_assoc[z,subsub[s1,s2]]⊗    ...by 2.5 and definition of @  

The result then follows from the second part of 2.12 and $NOTNIL-APPEND.  

.bb |Proof of 2.ii   ⊗⊗∀z_s1_s2:_sublis[z,s1@s2]_=_sublis[sublis[z,s1],s2]⊗.  |
Method: S-expression induction with ⊗⊗qP[z]_≡_∀s1_s2:_sublis[z,s1@s2]_=_sublis[sublis[z,s1],s2]⊗.

Case ⊗⊗qat z⊗:

    ⊗⊗sublis[z,s1@s2] = {assoc[z,s1@s2]}[λz1: qif qn z1 qthen z qelse qd z1]⊗
    ⊗⊗sublis[z,s1] = {assoc[z,s1]}[λz1: qif qn z1 qthen z qelse qd z1]⊗
.fill
If ⊗⊗qn assoc[z,s1]⊗ the result follows from 2.10 and if ⊗⊗¬qn assoc[z,s1]⊗
the result follows from 2.11.
.nofill

Case  ⊗⊗¬qat z⊗ and ⊗⊗∀s2: [sublis[qa z, s1@s2] = sublis[sublis[qa z,s1],s2]⊗
		∧ ⊗⊗∀s2: [sublis[qd z, s1@s2] = sublis[sublis[qd z,s1],s2]⊗

    ⊗⊗sublis[z,s1@s2] = sublis[qa z,s1@s2] . sublis[qd z,s1@s2]⊗   ...by definition
		    ⊗⊗= sublis[sublis[qa z,s1],s2] . sublis[sublis[qd z,si],s2]⊗    ...by induction
		    ⊗⊗= sublis[sublis[z,s1],s2]⊗   ... by definition of ⊗sublis 
           ...here we need ⊗⊗issexp sublis[qa z,s1]⊗ and ⊗⊗issexp sublis[qd z,s1]⊗ 


.bb |Proof of 2.iii ⊗⊗∀z s1 s2 s3: sublis[z, s1@[s2@s3]] = sublis[z, [s1@s2]@s3]]⊗ |
	This is a direct consequence of 2.ii and ⊗⊗slist s1@s2⊗ as follows:

		⊗⊗sublis[z, s1@[s2@s3]] = sublis[sublis[z,s1],s2@s3] ⊗
				⊗⊗= sublis[sublis[sublis[z,s1],s2],s3]⊗
				⊗⊗= sublis[sublis[z,s1@s2],s3]⊗
				⊗⊗= sublis[z, [s1@s2]@s3]⊗

.bb |Proof of 2.iv  ⊗⊗∀x y z: [¬occur[y,z] ⊃ subst[x,y,z] = z]⊗|
Method: S-expression induction with  ⊗⊗qP[z]_≡_∀x_y:_[¬occur[y,z]_⊃_subst[x,y,z]_=_z]⊗.  

Case ⊗⊗qat z⊗:

    ⊗⊗¬occur[y,z]_≡_y≠z⊗ and ⊗⊗subst[x,y,z]_=_qif_y_=_z_qthen_x_qelse_z⊗ so qP holds.  

Case ⊗⊗¬qat z⊗ and ⊗⊗∀x y: [¬occur[y, qa z] ⊃ subst[x,y,qa z] = qa z ∧  [¬occur[y, qd z] ⊃ subst [x,y,qd z]]⊗

    ⊗⊗¬occur[y,z]_≡_y≠z ∧ ¬occur[y,qa z]_∧_¬occur[y,qd z]⊗
    ⊗⊗subst[x,y,z]_=_subst[x,y,qa z]_._subst[x,y,qd z]⊗    ...by definition
                 ⊗⊗= qa z . qd z⊗   ...by induction hypothesis 
                 ⊗⊗= z⊗

%3Proof  of  2.v%1 ⊗⊗∀x  x1  y  y1  z:  [y ≠  y1  ∧  ¬occur[y,  x1]]  ⊃ ⊗
                                    ⊗⊗subst[x1,y1,subst[x,y,z] = subst[subst[x1,y1,x],y,subst[x1,y1,z]]⊗

Method: S-expression induction on ⊗z.  

Case ⊗⊗qat z⊗:

    ⊗⊗subst[x1,y1,subst[x,y,z]] = qif y=z qthen subst[x1,y1,x] qelse qif y1=z qthen x1 qelse z⊗

    ⊗⊗subst[subst[x1,y1,x],y,subst[x1,y1,z]] ⊗
		⊗⊗= qif y1=z qthen qif y=x1 qthen subst[x1,y1,x] qelse x1⊗
		            ⊗⊗qelse qif y=z qthen subst[x1,y1,x] qelse z⊗
		⊗⊗=qif y1=z qthen x1 qelse qif y=z qthen subst[x1,y1,x] qelse z⊗   ...since  ⊗⊗¬occur[y,x1]⊗

The result now follows by a simple case analysis since ⊗y=z and ⊗y1=z can not both be true.

Case ⊗⊗¬qat z⊗ and ⊗⊗∀x  x1  y  y1:  [y  ≠  y1  ∧  ¬occur[y,  x1]]  ⊃⊗
	⊗⊗subst[x1,y1,subst[x,y,qa z] = subst[subst[x1,y1,x],y,subst[x1,y1,qa z]]⊗
	⊗⊗∧ subst[x1,y1,subst[x,y,qd z] = subst[subst[x1,y1,x],y,subst[x1,y1,qd z]]]⊗ 

    ⊗⊗subst[x1,y1,subst[x,y,z]] = subst[x1,y1,subst[x,y,qa z] . subst[x,y,qd z]]⊗
		⊗⊗= subst[x1,y1,subst[x,y,qa z]] . subst[x1,y1,[subst[x,y,qd z]]⊗
                      ...here we need ⊗⊗issexp subst[x,y,qa z]⊗ and ⊗⊗issexp subst[x,y,qd z]⊗
		⊗⊗= subst[subst[x1,y1,x],y,subst[x1,y1,qa z]] . subst[subst[x1,y1,x],y,subst[x1,y1,qd z]]⊗
		⊗⊗= subst[subst[x1,y1,x],y,subst[x1,y1,z]]⊗

This completes problem 2.
.fill

.bb Problem 3.

	We wish to prove the following two statements:

(i)	⊗⊗∀u v: andlis[u*v,phi] ≡ andlis[u,phi] ∧ andlis[v,phi]⊗

(ii)	⊗⊗∀u: andlis[u,phi] ≡ andlis[reverse u,phi]⊗

where ⊗phi is a unary predicate.  (The use of ⊗p in the original porblem statement
was a poor choice as ⊗p is designated in Chapter 3 as a variable of type ⊗istv.)  
Note that even to state this problem requires
an extension to the syntax of our language in order to allow functions that
have functions as arguments.  In the problem ⊗phi is considered as a parameter.
(Quantification over predicates is not allowed.)

	The strategy for doing the proof is as follows.  We define an
imitation of ⊗andlis by the following axioms.
.nofill

3.1	⊗⊗∀u: [aandlis[u,pphi] = nnull u oor [pphi qa u aand aandlis[qd u,pphi]]⊗
3.2	⊗⊗∀u: isetv aandlis qd u⊗
3.3	⊗⊗∀u: isetv pphi qa u⊗
3.4	⊗⊗∀x: istv pphi x⊗
3.5	⊗⊗∀x: [phi x ≡ pphi x=$$TT$]⊗
3.6	⊗⊗∀u: [andlis[u,phi] ≡ aandlis[u,pphi] = $$TT$]⊗
.fill
Here ⊗nnull is defined similarly to ⊗aatom and we assume the analagous results 
such as $TVNNUL, and $EQNNUL.  
3.2 and 3.3 are needed inorder to be able
to use the definitions of ⊗aand and ⊗oor in the case ⊗⊗qn u⊗. 
Using these axioms we prove

3.7	⊗⊗∀u:_istv_aandlis[u,pphi]⊗ 

from which we get (using $EQAAND $EQOOR etc., and the above axioms)  that

3.8	⊗⊗∀u: [andlis[u,phi] ≡ qn u ∨ [phi qa u ∧ andlis[qd u,phi]]⊗.

This last statement is used together with list induction to prove the desired
results.
.nofill

.bb |Proof of 3.7 |
Method: list induction with ⊗⊗qP[u]_≡_istv_aandlis[u,pphi]⊗.
 
Case ⊗⊗qn u⊗:

    ⊗⊗aandlis[u,pphi]_=_$$TT$⊗   ...by  definitions of ⊗nnull, ⊗aand, ⊗oor, 3.1, 3.2 and 3.3 .  
    ⊗⊗istv_$$TT$⊗  

Case ⊗⊗¬qn u⊗  and ⊗⊗istv aandlis[qd u,pphi]⊗:

    ⊗⊗istv [pphi qa u aand aandlis[qd u,pphi]⊗   ...by induction, $TVAND and 3.4 
    ⊗⊗istv [nnull u]⊗   ..by remarks above
    ⊗⊗istv aandlis[u,pphi]⊗   ...by definition and $TVOOR.  

.bb |Proof of 3.i.|
Method: list induction with  ⊗⊗qP[u]_≡_∀v:_[andlis[u*v,phi]_≡_andlis[u,phi]_∧_andlis[v,phi]]⊗

Case ⊗⊗qn u⊗:

    ⊗⊗andlis[u*qNIL,phi] ≡ andlis[u,phi]⊗   ...by $NIL-APPEND  
                         ⊗⊗≡ andlis[u,phi] ∧ andlis[qNIL,phi]⊗  ...by 3.8

Case ⊗⊗¬qn u⊗ and ⊗⊗∀v: andlis[qd u*v,phi] ≡ andlis[qd u,phi] ∧ andlis[v,phi]⊗

    ⊗⊗andlis[u*v,phi] ≡ phi qa u ∧ andlis[qd u*v,phi]⊗    ...by $CAR/CDR-APPEND, $ISTOT-APPEND, and 3.8.
                ⊗⊗≡ phi qa u ∧ andlis[qd u,phi] ∧ andlis[v,phi]⊗    ...by the induction hypothesis
		⊗⊗≡ andlis[u,phi] ∧ andlis[v,phi]⊗    ...by 3.8.


.bb |Proof of 3.ii .|
Method: list induction with  ⊗⊗qP[u]_≡_[andlis[u,phi]_≡_andlis[reverse u,phi]]⊗.

Case ⊗⊗qn u⊗:

    ⊗⊗andlis[reverse qNIL,phi] ≡ andlis[qNIL,phi]⊗   ...by definition of ⊗reverse 

Case ⊗⊗¬qn u⊗ and ⊗⊗andlis[reverse qd u,phi] ≡ andlis[qd u,phi]⊗:

    ⊗⊗andlis[reverse u,phi] ≡ andlis[reverse qd u * <qa u>,phi]⊗    ...by definition of ⊗reverse 
		⊗⊗≡ andlis[reverse qd u,phi] ∧ andlis[<qa u>,phi]⊗    ...by (i) 
                        ...here we need ⊗⊗islist reverse qd u⊗ and ⊗⊗islist <qa u>⊗
		⊗⊗≡ andlis[<qa u>,phi] ∧ andlis[qd u,phi]⊗    ...by induction hypothesis
		⊗⊗≡ andlis[u,phi]⊗    ...by  3.8 and properties of <>.
.fill
This completes Problem 3.